es:event_system{i:l}, e:es-E(es).
(es-isrcv(es; e))  (loc(e) = destination(es-lnk(es; e))  Id) 

latex

Definitions	event_system{i:l}, t  T, x:A. B(x), es-E(es), es-isrcv(es; e), b, destination(l), loc(e), <a, b>, Id, s = t, void, x:AB(x), P  Q, False, A, x:A  B(x), let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , P  Q
Lemmas	es-axioms, es-loc-pred, assert wf, es-isrcv wf, es-E wf, event system wf